#pragma once

#include <iostream>
#include <shared_mutex>
#include <vector>

#define PAIR(a, b) \
  ((unsigned int)((((unsigned int)a) + ((unsigned int)b)) * (((unsigned int)a) + ((unsigned int)b) + ((unsigned int)1)) / ((unsigned int)2) + ((unsigned int)1)))
#define TRIPLE(a, b, c) ((unsigned int)(PAIR((unsigned int)c, PAIR(a, b))))

namespace nanobdd {

typedef int Bdd;

struct Node {
  uint32_t level;
  int low;
  int high;
  int hash;
  uint32_t next;
};

struct CacheEntry {
  int res;
  int a, b, c;
};

class Cache {
 public:
  Cache(size_t size) : cache_(size) {}

  int
  lookup(int hash, int x, int y, int op) {
    // std::shared_lock<std::shared_mutex> lock(mutex_);
    auto cache = cache_.at(hash);
    if (cache.a == x && cache.b == y && cache.c == op) {
      return cache.res;
    }
    return -1;
  }

  void
  insert(int hash, int res, int x, int y, int op) {
    // std::lock_guard<std::shared_mutex> lock(mutex_);
    // if (lookup(hash, x, y, op) != -1) {
    //   return;
    // }
    auto& cache = cache_.at(hash);
    cache.a = x;
    cache.b = y;
    cache.c = op;
    cache.res = res;
  }

 private:
  std::vector<CacheEntry> cache_;
  std::shared_mutex mutex_;
};

class Nanobdd {
 public:
  static inline int falseNode = 0;
  static inline int trueNode = 1;

  Nanobdd(size_t nodeSize, size_t cacheSize)
      : nodeSize_(nodeSize),
        cacheSize_(cacheSize),
        nodes_(nodeSize),
        cache_(cacheSize) {
    for (int i = 0; i < nodeSize; ++i) {
      auto& node = nodes_.at(i);
      node.low = -1;
      node.high = -1;
      node.next = i + 1;
    }
    nodes_.back().next = 0;

    nodes_[0].low = nodes_[0].high = 0;
    nodes_[1].low = nodes_[1].high = 1;
    freepos = 2;
  }

  void
  createVars(size_t varNum) {
    vars_.resize(varNum);
    for (int i = 0; i < varNum; ++i) {
      int v = makeNode(i, 0, 1);
      vars_[i] = v;
      makeNode(i, 1, 0);
    }
  }

  int
  getVar(uint32_t id) {
    return vars_[id];
  }

  int
  bddAnd(int x, int y) {
    if (x == y) {
      return x;
    }
    if (x == 0 || y == 0) {
      return 0;
    }
    if (x == 1) {
      return y;
    }
    if (y == 1) {
      return x;
    }
    auto hash = TRIPLE(x, y, 0) % cacheSize_;
    auto cache = cache_.lookup(hash, x, y, 0);
    if (cache != -1) {
      return cache;
    }

    auto m = std::min(nodes_[x].level, nodes_[y].level);

    auto fLow = bddAnd(negCof(x, m), negCof(y, m));
    auto fHigh = bddAnd(posCof(x, m), posCof(y, m));

    auto res = makeNode(m, fLow, fHigh);

    cache_.insert(hash, res, x, y, 0);

    return res;
  }

  int
  bddOr(int x, int y) {
    if (x == y) {
      return x;
    }
    if (x == 1 || y == 1) {
      return 1;
    }
    if (x == 0) {
      return y;
    }
    if (y == 0) {
      return x;
    }
    auto hash = TRIPLE(x, y, 1) % cacheSize_;
    auto cache = cache_.lookup(hash, x, y, 1);
    if (cache != -1) {
      return cache;
    }

    auto m = std::min(nodes_[x].level, nodes_[y].level);

    auto fLow = bddOr(negCof(x, m), negCof(y, m));
    auto fHigh = bddOr(posCof(x, m), posCof(y, m));

    auto res = makeNode(m, fLow, fHigh);

    cache_.insert(hash, res, x, y, 1);

    return res;
  }

  int
  bddNot(int x) {
    if (x == 0) {
      return 1;
    }
    if (x == 1) {
      return 0;
    }
    auto hash = x % cacheSize_;

    auto cache = cache_.lookup(hash, x, 0, 2);
    if (cache != -1) {
      return cache;
    }

    auto m = nodes_[x].level;

    auto fLow = bddNot(negCof(x, m));
    auto fHigh = bddNot(posCof(x, m));

    auto res = makeNode(m, fLow, fHigh);

    cache_.insert(hash, res, x, 0, 2);

    return res;
  }

 private:
  int
  negCof(int x, uint32_t id) {
    if (id < nodes_[x].level) {
      return x;
    } else { // id == root_
      return nodes_[x].low;
    }
  }

  int
  posCof(int x, uint32_t id) const {
    // check id <= root_
    if (id < nodes_[x].level) {
      return x;
    } else { // id == root_
      return nodes_[x].high;
    }
  }

  int
  makeNode(uint32_t level, int low, int high) {
    if (low == high) {
      return low;
    }

    auto hash = TRIPLE(level, low, high) % nodeSize_;

    {
      // std::shared_lock<std::shared_mutex> lock(mutex_);
      auto res = nodes_[hash].hash;
      while (res != 0) {
        if (nodes_[res].level == level && nodes_[res].low == low &&
            nodes_[res].high == high) {
          return res;
        }
        res = nodes_[res].next;
      }
    }

    if (freepos == 0) {
      std::cout << "No space" << std::endl;
    }

    // std::lock_guard<std::shared_mutex> lock(mutex_);
    // search node again 
    // auto res = nodes_[hash].hash;
    // while (res != 0) {
    //   if (nodes_[res].level == level && nodes_[res].low == low &&
    //       nodes_[res].high == high) {
    //     return res;
    //   }
    //   res = nodes_[res].next;
    // }

    // create new node
    mutex_.lock();
    auto res = freepos;
    freepos = nodes_[freepos].next;
    mutex_.unlock();
    auto& node = nodes_.at(res);
    node.level = level;
    node.low = low;
    node.high = high;

    node.next = nodes_[hash].hash;
    nodes_[hash].hash = res;

    return res;
  }

  size_t nodeSize_;
  size_t cacheSize_;
  std::vector<Node> nodes_;
  int freepos;
  std::vector<int> vars_;
  Cache cache_;
  std::shared_mutex mutex_;
};

} // namespace nanobdd